Definitions | ff, tt, i <z j,  b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), lelt(i; j; k), Y, ||as||, int_seg(i; j), l[i], False, A, A B, A c B, x:A. B(x), guard(T), P Q, (x l), prop{i:l}, P  Q, P Q,  x. t(x), top, P  Q, x(s), P   Q, t T, x:A. B(x),  |